Lean勉強会 2023-12-10
15:00～16:00
Lean is based on a version of dependent type theory known as the Calculus of Constructions, with a countable hierarchy of non-cumulative universes and inductive types 日本語訳: Leanは非累積的宇宙と帰納的型の可算階層を持つ、構成的計算として知られる依存型理論のバージョンに基づいている。 ここで言及されている宇宙(universe)はグロタンディーク宇宙ではなく型宇宙(type universe)？ #xxxxxはコマンド
#checkコマンドは型を調べるやつ？
#evalコマンドで評価する
TypeはType 0の略である
#check TypeをするとType 0の型の型になって+1される
code:memo
#check Type 0 --> Type : Type 1 #check Type 1 --> Type : Type 2 universe uのようにuniverseコマンドを使いたくない場合は以下のような記法を使う
code:memo
def F.{u} (α : Type u) : Type u := Prod α α
17:00～18:00
今日読んだのは以下
以下メモ
============================
LazyComputationはそのまま訳すと遅延計算
lctxはlocal context
MetaM: メタ変数のモナド？
ContextInfo.save
code:src/lean/Lean/Elab/InfoTree/Main.lean
let ctx ← saveNoFileMap
return { ctx with fileMap := (← getFileMap) }
end ContextInfo
Lean 4は正格評価の言語
runnerWidget
mkprocsコマンド？でRpcEncodableになっている
RunnerWidgetPropsは19行目で#mkrpcencコマンドで定義されている
code:memo
-- Make it possible for widgets to receive RunnerWidgetProps. Uses the TypeName instance.
instance : RpcEncodable (LazyEncodable Json)が定義されている
structureの型がRpcEncodableと定義しているっぽい